#pragma once

/**********************************************************
oxsat - portable sat solver for windows and unix
Copyright (C) 2017  tj bandrowsky

This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
*/


#include "skip_list2.h"
#include "clause.h"
#include <list>
#include <algorithm>
#include <string>

namespace solver
{
	class decision
	{
	public:
		int selected_literal;
		std::vector<literal> literals;
		int line_number;
	};

	typedef decision *pdecision;

	typedef skip_lists::skip_list_type<int, literal, skip_lists::int_compare_type> decision_list;
	typedef skip_lists::skip_list_type<int, literal, skip_lists::int_compare_type>::node_type decision_node;

	class decision_string 
	{
		decision_list items;

	public:

		bool is_c_str;

		decision_string() : is_c_str(false), items(0, literal())
		{

		}

		decision_string( const char *mystr ) : is_c_str(true), items(0, literal())
		{
			literal lit;
			int val = 1;
			bool star = false;

			while (*mystr)
			{

				switch (*mystr) 
				{
				case 'A':
				case 'B':
				case 'C':
				case 'D':
				case 'E':
				case 'F':
				case 'G':
				case 'H':
				case 'I':
				case 'J':
				case 'K':
				case 'L':
				case 'M':
				case 'N':
				case 'O':
				case 'P':
				case 'Q':
				case 'R':
				case 'S':
				case 'T':
				case 'U':
				case 'V':
				case 'W':
				case 'X':
				case 'Y':
				case 'Z':
					lit.ref = *mystr;
					lit.val = val;
					val = 1;
					star = false;
					items.update(lit.ref, lit);
					break;
				case '*':
					star = true;
					val = -1;
					break;
				case '!':
					val = !val;
					break;
				}

				if (*mystr) 
				{
					mystr++;
				}
			}
		}

		decision_string(const decision_string& src) :items( src.items ), is_c_str( src.is_c_str )
		{
		}

		void operator = (decision_string& src)
		{
			is_c_str = src.is_c_str;
			items = src.items;
		}

		inline int size()
		{
			return items.size();
		}

		decision_node *first()
		{
			return items.first();
		}

		decision_node *next(decision_node *n)
		{
			return items.next(n);
		}

		void clear()
		{
			items.clear();
		}

		bool exists(literal l)
		{
			bool found = false;

			auto n = items.find( l.ref );

			found = n != nullptr;
			
			return found;
		}

		bool exists_exact(literal l)
		{
			bool found = false;

			auto n = items.find(l.ref);

			found = n != nullptr && n->value == l;

			return found;
		}

		bool remove(literal lit)
		{
			bool removed = items.remove(lit.ref);
			return removed;
		}

		bool remove(decision_string& s)
		{
			bool removed = false;
			for (auto sn = s.first(); sn != nullptr; sn = s.next(sn))
			{
				if (remove(sn->value))
				{
					removed = true;
				}
			}
			return removed;
		}

		void add(decision_string& s)
		{
			for (auto nd = s.first(); nd != nullptr; nd = s.next(nd))
			{
				add(nd->value);
			}
		}

		bool compatible(decision_string& s)
		{
			for (auto nd = s.first(); nd != nullptr; nd = s.next(nd))
			{
				auto n = items.find(nd->value.ref);
				if (n != nullptr && n->value.val != nd->value.val)
					return false;
			}
			return true;
		}

		bool contains(decision_string& s)
		{
			bool all_found = true;
			for (auto nd = s.first(); nd != nullptr; nd = s.next(nd))
			{
				if (!exists(nd->value)) 
				{
					all_found = false;
					break;
				}
			}
			return all_found;
		}

		bool joins(decision_string& s)
		{
			for (auto nd = s.first(); nd != nullptr; nd = s.next(nd))
			{
				if (exists(nd->value))
				{
					return true;
				}
			}
			return false;
		}

		bool add(literal l)
		{
			bool added = false;

			auto n = items.find(l.ref);

			if (n) 
			{
				if (n->value == l)
				{
					added = true;
				}
				else 
				{
					added = false;
				}
			} 
			else 
			{
				added = items.update(l.ref, l );
			}

			return added;
		}

		void fold(decision_string& str)
		{
			auto n = str.first();
			while (n != nullptr)
			{
				auto y = items.find(n->key);
				if (y != nullptr)
				{
					y->value = n->value;
				}
				else 
				{
					add(n->value);
				}
				n = str.next(n);
			}
		}
		
		decision_string *clone()
		{
			decision_string *ds = new decision_string(*this);
			return ds;
		}

		literal *find(int ref)
		{
			auto n = items.find(ref);
			return n != nullptr ? &(n->value) : (literal *)nullptr;
		}

		decision_node *find_node(int ref)
		{
			auto n = items.find(ref);
			return n;
		}

	};

	typedef decision_string *pdecision_string;

}
